$\forall$$T$:Type, $f$:($\mathbb{N}\rightarrow$$T$), $s$:($k$:$\mathbb{N}\times$($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow\mathbb{N}$)). derived{-}seq($f$;$s$) $\in$ $\mathbb{N}\rightarrow$$k$:$\mathbb{N}\times$($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow$$T$)